p,q:. ((p q))  ((p)  (q)) 

latex

ProofTree

Definitions	t  T, x:A. B(x), ff, , P  Q, P  Q, P  Q, True, if b then t else f fi , tt, P  Q, p q, b, P  Q, False, Unit, ,
Lemmas	bool wf, false wf, true wf